/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓Introduction and Motivation

␈↓ α∧␈↓␈↓ αTThis␈αpaper␈αadvances␈αtwo␈αaspects␈αof␈αthe␈αstudy␈αof␈αthe␈αproperties␈αof␈αcomputer␈αprograms␈α-␈αthe
␈↓ α∧␈↓scientifically␈α
motivated␈α
search␈α
for␈α
general␈αtheorems␈α
that␈α
permit␈α
deducing␈α
properties␈α
of␈αprograms
␈↓ α∧␈↓and␈α∩the␈α∩engineering␈α∩problem␈α∩of␈α∩replacing␈α∩debugging␈α∩by␈α∩computer-assisted␈α∩computer-checked
␈↓ α∧␈↓proofs␈α∂that␈α∂programs␈α∞have␈α∂desired␈α∂properties.␈α∞ Both␈α∂tasks␈α∂require␈α∞mathematics,␈α∂but␈α∂the␈α∞second
␈↓ α∧␈↓also␈α
requires␈αkeeping␈α
a␈αnon-mathematical␈α
goal␈αin␈α
mind.␈α
 In␈αparticular,␈α
it␈αis␈α
easy␈αfor␈α
the␈αtheorist␈α
to
␈↓ α∧␈↓neglect␈αto␈αgive␈αan␈αestimate␈α
of␈αthe␈αrange␈αof␈αapplicability␈α
of␈αhis␈αtheorems␈αand␈αexamples␈α
that␈αshow
␈↓ α∧␈↓how to use them.

␈↓ α∧␈↓␈↓ αTCartwright␈α(1976)␈αshows␈αhow␈αa␈αrecursive␈αprogram␈α(as␈αin␈αpure␈αLisp)␈αdefines␈αa␈αfunction␈αin␈αa
␈↓ α∧␈↓first␈α∀order␈α∀theory.␈α∀ The␈α∀function␈α∀satisfies␈α∪a␈α∀␈↓↓functional␈α∀equation␈↓␈α∀trivially␈α∀obtained␈α∀from␈α∪the
␈↓ α∧␈↓program,␈α∞and␈α∞if␈α∞the␈α∂program␈α∞always␈α∞terminates,␈α∞the␈α∂functional␈α∞equation␈α∞has␈α∞a␈α∂unique␈α∞solution.
␈↓ α∧␈↓One␈α⊂result␈α⊂of␈α⊂this␈α⊂paper␈α⊂shows␈α⊂that␈α⊂supplementing␈α⊂the␈α⊂␈↓↓functional␈α⊂equation␈↓␈α⊂by␈α⊃a␈α⊂␈↓↓minimization
␈↓ α∧␈↓↓schema␈↓.␈α
 As␈α
is␈α∞shown␈α
in␈α
(Cartwright␈α∞and␈α
McCarthy␈α
1979)␈α∞this␈α
completes␈α
the␈α∞characterization␈α
of
␈↓ α∧␈↓recursively␈α
defined␈α
programs.␈α∞ Namely,␈α
given␈α
the␈α∞functional␈α
equation␈α
and␈α∞minimization␈α
schema,
␈↓ α∧␈↓any␈α
sentence␈α
involving␈α
the␈α
function␈α
defined␈α
by␈αthe␈α
program␈α
can␈α
be␈α
proved␈α
within␈α
first␈αorder␈α
logic
␈↓ α∧␈↓to␈α⊂be␈α∂equivalent␈α⊂to␈α⊂a␈α∂sentence␈α⊂not␈α⊂involving␈α∂the␈α⊂function,␈α∂i.e.␈α⊂a␈α⊂sentence␈α∂in␈α⊂the␈α⊂data␈α∂domain.
␈↓ α∧␈↓Therefore,␈α↔inability␈α↔to␈α_prove␈α↔or␈α↔disprove␈α_termination␈α↔is␈α↔just␈α_a␈α↔matter␈α↔of␈α_the␈α↔G␈↓
:␈↓odelian
␈↓ α∧␈↓incompleteness␈α
and␈αundecideability␈α
of␈α
the␈αdata␈α
domain.␈α
 (It␈αis␈α
required␈α
that␈αthe␈α
data␈αdomain␈α
have
␈↓ α∧␈↓enough functions for elementary syntax).

␈↓ α∧␈↓␈↓ αTWhile␈α
we␈αshall␈α
prove␈αsome␈α
theoretical␈α
results␈αand␈α
cite␈αothers,␈α
the␈α
main␈αcontent␈α
of␈αthis␈α
paper
␈↓ α∧␈↓is a discussion of the application of these new methods to the verification of recursive programs.



␈↓ α∧␈↓Two Inessential Extensions to First Order Logic

␈↓ α∧␈↓␈↓ αTWe␈α
begin␈α
by␈α
extending␈α
first␈α
order␈α
logic␈α
to␈α
include␈α
conditional␈α
expressions␈α
and␈α
first␈αorder␈α
λ-
␈↓ α∧␈↓expressions.␈α Translating␈αrecursive␈αprograms␈αinto␈αlogical␈αsentences␈αcould␈αbe␈αaccomplished␈αwithout
␈↓ α∧␈↓these␈α
extensions,␈αbut␈α
the␈αresulting␈α
sentences␈αwould␈α
often␈αbe␈α
much␈αlonger␈α
than␈αthe␈α
programs␈αand
␈↓ α∧␈↓their␈α∪relation␈α∪to␈α∪the␈α∪program␈α∪would␈α∪be␈α∪obscured.␈α∪ Since␈α∪we␈α∪are␈α∪creating␈α∪tools␈α∀for␈α∪proving
␈↓ α∧␈↓properties␈α
of␈α
actual␈α
programs,␈α
we␈α
must␈α
face␈α
the␈α
fact␈α
that␈α
useful␈α
programs␈α
are␈α
quite␈α
long␈α
enough␈α
as
␈↓ α∧␈↓it␈α
is.␈α∞ Obscuring␈α
their␈α∞content␈α
in␈α∞the␈α
course␈α∞of␈α
translating␈α∞them␈α
into␈α∞logic␈α
might␈α∞make␈α
program
␈↓ α∧␈↓proving␈αimpractical␈αor␈αat␈αleast␈αmuch␈αmore␈αdifficult.␈α On␈αthe␈αother␈αhand,␈αwe␈αcannot␈αadd␈αarbitrary
␈↓ α∧␈↓programming␈α∪constructions␈α∪to␈α∪first␈α∪order␈α∀logic␈α∪without␈α∪risking␈α∪its␈α∪useful␈α∪properties␈α∀such␈α∪as
␈↓ α∧␈↓completeness.␈α∞ Fortunately,␈α∞these␈α∞are␈α∞harmless␈α∞and␈α∞generally␈α∞useful␈α∞extensions.␈α∞ In␈α∞fact,␈α∞they␈α∞are
␈↓ α∧␈↓useful␈α_for␈α_expressing␈α_mathematical␈α_ideas␈α_concisely␈α_and␈α_understandably␈α_quite␈α_apart␈α_from
␈↓ α∧␈↓applications␈α∀to␈α∀computer␈α∃science.␈α∀ The␈α∀reader␈α∃is␈α∀assumed␈α∀to␈α∃know␈α∀about␈α∀first␈α∃order␈α∀logic,
␈↓ α∧␈↓conditional expressions and λ-expressions; we explain only their connection.

␈↓ α∧␈↓␈↓ αTRemember␈αthat␈αthe␈α
syntax␈αof␈αfirst␈α
order␈αlogic␈αis␈αgiven␈α
in␈αthe␈αform␈α
of␈αrecursive␈αrules␈αfor␈α
the
␈↓ α∧␈↓formation of terms and wffs.  The rule for forming terms is extended as follows:

␈↓ α∧␈↓␈↓ αTIf␈α∞␈↓↓p␈↓␈α
is␈α∞a␈α∞wff␈α
and␈α∞␈↓↓a␈↓␈α
and␈α∞␈↓↓b␈↓␈α∞are␈α
terms,␈α∞then␈α∞␈↓↓IF␈α
p␈α∞THEN␈α
a␈α∞ELSE␈α∞b␈↓␈α
is␈α∞a␈α∞term.␈α
 Sometimes
␈↓ α∧␈↓parentheses must be added to insure unique decomposition.

␈↓ α∧␈↓␈↓ αTThe␈α⊂semantics␈α⊂of␈α⊂conditional␈α⊃expression␈α⊂terms␈α⊂is␈α⊂given␈α⊃by␈α⊂a␈α⊂rule␈α⊂for␈α⊃determining␈α⊂their
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓values.␈α
 Namely,␈αif␈α
␈↓↓p␈↓␈α
is␈αtrue,␈α
the␈α
the␈αvalue␈α
of␈α
␈↓↓IF␈αp␈α
THEN␈α
a␈αELSE␈α
b␈↓␈α
is␈αthe␈α
value␈α
of␈α␈↓↓a.␈↓␈α
Otherwise
␈↓ α∧␈↓it is the value of ␈↓↓b.␈↓

␈↓ α∧␈↓␈↓ αTIt␈α∪is␈α∪also␈α∪necessary␈α∪to␈α∪add␈α∪rules␈α∪of␈α∪inference␈α∪to␈α∪the␈α∪logic␈α∪concerned␈α∪with␈α∩conditional
␈↓ α∧␈↓expressions.␈α∞ One␈α∂could␈α∞get␈α∂by␈α∞with␈α∞rules␈α∂permitting␈α∞the␈α∂elimination␈α∞of␈α∂conditional␈α∞expressions
␈↓ α∧␈↓from␈α∂sentences␈α∞and␈α∂their␈α∞introduction.␈α∂ These␈α∞rules␈α∂are␈α∞important␈α∂anyway,␈α∞because␈α∂they␈α∞permit
␈↓ α∧␈↓proof␈α⊂of␈α⊂the␈α⊂metatheorem␈α⊃that␈α⊂the␈α⊂main␈α⊂properties␈α⊂of␈α⊃first␈α⊂order␈α⊂logic␈α⊂are␈α⊂unaffected␈α⊃by␈α⊂the
␈↓ α∧␈↓addition␈α∩of␈α⊃conditional␈α∩expressions.␈α∩ These␈α⊃include␈α∩completeness,␈α⊃the␈α∩deduction␈α∩theorem,␈α⊃and
␈↓ α∧␈↓semi-decidability.

␈↓ α∧␈↓␈↓ αTIn␈α
order␈α
to␈α
state␈α
these␈α
rules␈α
it␈α
is␈α
convenient␈α
to␈α
introduce␈α
conditional␈α
expressions␈α
also␈α∞as␈α
a
␈↓ α∧␈↓ternary␈αlogical␈αconnective.␈α A␈α
more␈αfastidious␈αexposition␈αwould␈α
use␈αa␈αdifferent␈αnotation␈αfor␈α
logical
␈↓ α∧␈↓conditional␈αexpressions,␈αbut␈αwe␈α
will␈αuse␈αthem␈αso␈α
little␈αthat␈αwe␈αmight␈α
as␈αwell␈αuse␈αthe␈αsame␈α
notation,
␈↓ α∧␈↓especially␈αsince␈α
it␈αis␈α
not␈αambiguous.␈α
 Namely,␈αif␈α
␈↓↓p,␈↓␈α␈↓↓q,␈↓␈αand␈α
␈↓↓r␈↓␈αare␈α
wffs,␈αthen␈α
so␈αis␈α
␈↓↓IF␈αp␈α
THEN␈αq
␈↓ α∧␈↓↓ELSE␈α∩r␈↓.␈α∪ Its␈α∩semantics␈α∪is␈α∩given␈α∩by␈α∪considering␈α∩it␈α∪as␈α∩a␈α∪synonym␈α∩for␈α∩␈↓↓((p␈α∪∧␈α∩q)␈α∪∨␈α∩(¬p␈α∪∧␈α∩r))␈↓.
␈↓ α∧␈↓Elimination of conditional expressions is made possible by the distributive laws

␈↓ α∧␈↓1)␈↓ αt ␈↓↓f(IF p THEN a ELSE b) = IF p THEN f(a) ELSE f(b)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓2)␈↓ αt  ␈↓↓P(IF p THEN a ELSE b)␈↓ ¬T≡ IF p THEN P(a) ELSE P(b)␈↓

␈↓ α∧␈↓␈↓ ¬T≡ (p ∧ P(a)) ∨ (¬p ∧ P(b))

␈↓ α∧␈↓where␈α∞␈↓↓f␈↓␈α∞and␈α∞␈↓↓P␈↓␈α∞stand␈α∞for␈α∞arbitrary␈α∞function␈α∞and␈α∞predicate␈α∞symbols␈α∂respectively.␈α∞ Corresponding
␈↓ α∧␈↓distributive␈α
rules␈α
are␈α
needed␈αfor␈α
functions␈α
and␈α
predicates␈α
of␈αseveral␈α
arguments␈α
when␈α
one␈α
of␈αthe
␈↓ α∧␈↓arguments is a conditional expression.

␈↓ α∧␈↓␈↓ αTNotice␈α
that␈α
this␈αaddition␈α
to␈α
the␈αlogic␈α
has␈α
nothing␈αto␈α
do␈α
with␈αpartial␈α
functions␈α
or␈αthe␈α
element
␈↓ α∧␈↓␈↓πT␈↓.

␈↓ α∧␈↓␈↓ αTWhile␈αthe␈αabove␈αrules␈αare␈αsufficient␈αto␈αpreserve␈αthe␈αcompleteness␈αof␈αfirst␈αorder␈αlogic,␈αproofs
␈↓ α∧␈↓are␈α∂often␈α∂greatly␈α⊂shortened␈α∂by␈α∂using␈α⊂the␈α∂additional␈α∂rules␈α⊂introduced␈α∂in␈α∂(McCarthy␈α⊂1963).␈α∂ We
␈↓ α∧␈↓mention␈α
especially␈α
an␈α
extended␈α
form␈α
of␈αthe␈α
rule␈α
for␈α
replacing␈α
an␈α
expression␈α
by␈αanother␈α
expression
␈↓ α∧␈↓proved␈α
equal␈αto␈α
it.␈α Suppose␈α
we␈αwant␈α
to␈αreplace␈α
the␈αexpression␈α
␈↓↓c␈↓␈αby␈α
an␈αexpression␈α
␈↓↓c'␈↓␈α
within␈αthe
␈↓ α∧␈↓conditional␈αexpression␈α␈↓↓IF␈αp␈αTHEN␈αa␈αELSE␈αb␈↓.␈α To␈αreplace␈αan␈αoccurrence␈αof␈α␈↓↓c␈↓␈αwithin␈α␈↓↓a,␈↓␈αwe␈αneed
␈↓ α∧␈↓not␈αprove␈α
␈↓↓c = c'␈↓␈αbut␈α
merely␈α␈↓↓p ⊃ c = c'␈↓.␈α
 Likewise␈αif␈αwe␈α
want␈αto␈α
replace␈αan␈α
occurrence␈αof␈α
␈↓↓c␈↓␈αin␈α␈↓↓b,␈↓␈α
we
␈↓ α∧␈↓need only prove ␈↓↓¬p ⊃ c = c'␈↓.  This principle is further extended in the afore-mentioned paper.

␈↓ α∧␈↓␈↓ αTA␈αfurther␈αuseful␈αand␈α
eliminable␈αextension␈αto␈αthe␈αlogic␈α
is␈αto␈αallow␈α"first␈αorder"␈α
λ-expressions
␈↓ α∧␈↓as␈αfunction␈αand␈α
predicate␈αexpressions.␈α Thus␈α
if␈α␈↓↓x␈↓␈αis␈α
an␈αindividula␈αvariable,␈α
␈↓↓e␈↓␈αis␈αa␈α
term,␈αand␈α␈↓↓p␈↓␈αis␈α
a
␈↓ α∧␈↓wff,␈α
then␈α␈↓↓λx.e␈↓␈α
and␈α
␈↓↓λx.p␈↓␈αmay␈α
be␈α
used␈αwherever␈α
a␈α
function␈αsymbol␈α
or␈α
predicate␈αsymbol␈α
respectively
␈↓ α∧␈↓are␈αallowed.␈α The␈αonly␈αrule␈αrequired␈αis␈αlambda␈αconversion␈αwhich␈αserves␈αto␈αeliminate␈αor␈αintroduce
␈↓ α∧␈↓λ-expressions.␈α
 (We␈αassume␈α
that␈αthe␈α
rules␈αfor␈α
λ-conversion␈αinclude␈α
alphabetic␈αchanges␈α
of␈αbound
␈↓ α∧␈↓variables when needed to avoid capture of the free variables in arguments of λ-expressions.

␈↓ α∧␈↓␈↓ αTThe␈αuse␈α
of␈αminimization␈αschemata␈α
and␈αschemata␈αof␈α
induction␈αis␈αfacilitated␈α
by␈αfirst␈αorder␈α
λ-
␈↓ α∧␈↓exressions,␈αsince␈αthe␈α
substitution␈αjust␈αreplaces␈α
occurrences␈αof␈αthe␈α
function␈αvariable␈αin␈α
the␈αschema
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓by␈αa␈αλ-expression␈αwhich␈αcan␈αsubsequently␈αbe␈αexpanded␈αby␈αλ-conversion.␈α Without␈αλ-expressions
␈↓ α∧␈↓the␈αrule␈αfor␈αsubstitution␈αin␈αschemata␈αis␈αcomplicated␈αto␈αstate.␈α First␈αorder␈αλ-expressions␈αalso␈αpermit
␈↓ α∧␈↓many␈α⊂sentences␈α⊃to␈α⊂be␈α⊂expressed␈α⊃more␈α⊂compactly␈α⊂as␈α⊃well␈α⊂as␈α⊂being␈α⊃required␈α⊂to␈α⊃avoid␈α⊂duplicate
␈↓ α∧␈↓computations␈α~in␈α~recursive␈α~programs.␈α~ Thus␈α~we␈α~can␈α~write␈α~␈↓↓[λx.x↑2 + x](a + b)␈↓␈α≠instead␈α~of
␈↓ α∧␈↓␈↓↓(a + b)↑2 + (a + b)␈↓.␈α Since␈αall␈αoccurrences␈αof␈αfirst␈αorder␈αλ-expressions␈αcan␈αbe␈αeliminated␈αfrom␈αwffs
␈↓ α∧␈↓by␈αlambda␈αconversion,␈αthe␈αmetatheorems␈αof␈αfirst␈αorder␈αlogic␈αare␈αagain␈αpreserved.␈α The␈αreason␈αwe
␈↓ α∧␈↓don't␈αget␈αthe␈αfull␈αlambda␈αcalculus␈αis␈αthat␈αthe␈αsyntactic␈αrules␈αof␈αfirst␈αorder␈αlogic␈αprevent␈αa␈αvariable
␈↓ α∧␈↓from␈α∞being␈α∞used␈α∞in␈α
both␈α∞term␈α∞and␈α∞function␈α
positions.␈α∞ While␈α∞we␈α∞have␈α
illustrated␈α∞the␈α∞use␈α∞of␈α
λ-
␈↓ α∧␈↓expressions␈αwith␈αsingle␈αvariable␈αλ's,␈αexpressions␈αlike␈α␈↓↓λx y z.e␈↓␈αare␈αalso␈αuseful␈αand␈αgive␈αno␈αtrouble.
␈↓ α∧␈↓Partial Predicates

␈↓ α∧␈↓␈↓ αTWe␈α
have␈α
discussed␈α
treating␈αpartial␈α
functions␈α
by␈α
introducing␈α
␈↓πT␈↓.␈α A␈α
function␈α
take␈α
the␈αvalue␈α
␈↓πT␈↓
␈↓ α∧␈↓when␈α∞the␈α∞program␈α∞that␈α∞computes␈α∞it␈α∞doesn't␈α∞terminate,␈α∞and␈α∞it␈α∞is␈α∞sometimes␈α∞convenient␈α∞to␈α∂give␈α∞a
␈↓ α∧␈↓function the value ␈↓πT␈↓ in some other cases when we want it to be undefined.

␈↓ α∧␈↓␈↓ αTPartial␈α⊂predicates␈α⊂give␈α∂rise␈α⊂to␈α⊂new␈α∂problems.␈α⊂ The␈α⊂computation␈α∂of␈α⊂a␈α⊂recursively␈α∂defined
␈↓ α∧␈↓predicate␈αmay␈αnot␈αterminate,␈αso␈αthe␈αsame␈α
problem␈αarises.␈α However,␈αwe␈αcan't␈αsolve␈αit␈αin␈α
the␈αsame
␈↓ α∧␈↓way␈αwithout␈αadding␈α
an␈αadditional␈αundefined␈α
truth␈αvalue␈αto␈α
the␈αlogic.␈α This␈α
would␈αgive␈αrise␈α
to␈αa
␈↓ α∧␈↓partial␈α⊂first␈α∂order␈α⊂logic␈α∂in␈α⊂which␈α⊂sentences␈α∂could␈α⊂be␈α∂true,␈α⊂false␈α∂or␈α⊂undefined.␈α⊂ Various␈α∂partial
␈↓ α∧␈↓predicate␈αcalculi␈αhave␈αbeen␈αstudied␈αin␈α(McCarthy␈α1964)␈αand␈αelsewhere,␈αbut␈αthey␈αhave␈αthe␈αserious
␈↓ α∧␈↓disadvantage␈α⊂that␈α⊂arguments␈α⊂by␈α⊂cases␈α⊂become␈α⊂quite␈α⊂long,␈α⊂since␈α⊂three␈α⊂cases␈α⊂always␈α⊂have␈α⊂to␈α∂be
␈↓ α∧␈↓provided␈α
for,␈α
even␈α
when␈α
most␈α
of␈α
the␈α
predicates␈α
are␈α
known␈α
to␈α
be␈α
total.␈α
 Moreover,␈α
existing␈αlogic
␈↓ α∧␈↓texts,␈α∞proof-checkers␈α
and␈α∞theorem␈α
provers␈α∞all␈α
use␈α∞total␈α
logic.␈α∞ Therefore,␈α
it␈α∞seems␈α
better␈α∞to␈α
keep
␈↓ α∧␈↓the logic conventional and handle partial predicates as functions.

␈↓ α∧␈↓␈↓ αTWe␈αintroduce␈αa␈αdomain␈α␈↓	P␈↓␈αwith␈αthree␈αelements␈α␈↓↓T,␈↓␈α␈↓↓F␈↓␈αand␈α␈↓πT␈↓␈αcalled␈αthe␈αdomain␈αof␈αextended
␈↓ α∧␈↓truth␈α
values.␈α
 In␈α
a␈α
sorted␈α
logic,␈α
this␈α
may␈α
be␈α
a␈α
separate␈α
sort.␈α
 Otherwise,␈α
it␈α
may␈α
be␈αconsidered␈α
either
␈↓ α∧␈↓separately␈α∞or␈α
as␈α∞part␈α∞of␈α
the␈α∞main␈α∞data␈α
domain.␈α∞ In␈α
Lisp␈α∞it␈α∞is␈α
convenient␈α∞to␈α∞regard␈α
␈↓↓T␈↓␈α∞and␈α∞␈↓↓F␈↓␈α
as
␈↓ α∧␈↓special␈α
atoms␈α
and␈α
to␈α
use␈α
the␈α
same␈α
␈↓πT␈↓␈α
for␈α
extended␈α
truth␈α
values␈α
as␈α
for␈α
extended␈α
S-expressions.␈α It␈α
is
␈↓ α∧␈↓even␈αpossible␈αto␈α
follow␈αthe␈αLisp␈α
implementations␈αthat␈αuse␈α
qNIL␈αfor␈α␈↓↓F␈↓␈α
and␈αinterpret␈αall␈α
other␈αS-
␈↓ α∧␈↓expressions as ␈↓↓T,␈↓ although we don't to that in this paper.

␈↓ α∧␈↓␈↓ αTFor␈α⊃every␈α⊃predicate␈α⊃or␈α⊃boolean␈α⊃operator,␈α⊃we␈α⊃introduce␈α⊃a␈α⊃corresponding␈α∩function␈α⊃taking
␈↓ α∧␈↓taking␈α
an␈α
extended␈α
truth␈α
value␈α
as␈α
its␈α
value.␈α
 For␈α
example,␈α
we␈α
have␈α
a␈α
function␈α
␈↓↓and␈↓␈α
written␈αwith␈α
an
␈↓ α∧␈↓infix and defined by

␈↓ α∧␈↓␈↓ αT␈↓↓p and q = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN q ELSE F␈↓.

␈↓ α∧␈↓The␈αfunction␈α␈↓↓and␈↓␈αis␈αdistinct␈αfrom␈αthe␈αlogical␈αoperator␈α∧␈αwhich␈αremains␈αin␈αthe␈αlogic.␈α To␈αillustrate
␈↓ α∧␈↓this, we have the sentence

␈↓ α∧␈↓␈↓ αT␈↓↓((p and q) = T) ≡ (p = T) ∧ (q = T).

␈↓ α∧␈↓The␈α
parentheses␈α
in␈α
the␈α
above␈α
can␈αbe␈α
omitted␈α
without␈α
ambiguity␈α
given␈α
suitable␈α
preference␈αrules.
␈↓ α∧␈↓Note␈αthat␈α␈↓↓and␈↓␈αhas␈αthe␈αnon-commutative␈αproperty␈αof␈α(McCarthy␈α1963),␈αnamely␈α␈↓↓F and ␈↓πT␈↓↓ = F␈↓␈α
while
␈↓ α∧␈↓␈↓↓␈↓πT␈↓↓ and F = ␈↓πT␈↓↓␈↓.␈α∂ The␈α⊂this␈α∂corresponds␈α∂to␈α⊂the␈α∂fact␈α∂that␈α⊂it␈α∂is␈α∂convenient␈α⊂to␈α∂compute␈α∂␈↓↓p and q␈↓␈α⊂by␈α∂a
␈↓ α∧␈↓program␈α
that␈α
doesn't␈α
look␈α
at␈α
␈↓↓q␈↓␈αif␈α
␈↓↓p␈↓␈α
is␈α
false␈α
but␈α
which␈αdoesn't␈α
terminate␈α
if␈α
the␈α
computation␈α
of␈α␈↓↓p␈↓
␈↓ α∧␈↓doesn't␈αterminate.␈α Symmetry␈αcould␈αbe␈αrestored␈αif␈αthe␈αcomputer␈αtime-shared␈αits␈αcomputations␈αof␈α␈↓↓p␈↓
␈↓ α∧␈↓and␈α␈↓↓q,␈↓␈αbut␈αthere␈αare␈αtoo␈αmany␈αpractical␈αdisadvantages␈αto␈αsuch␈αa␈αsystem␈αto␈αjustify␈αdoing␈αit␈αfor␈αthe
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓sake␈α∪of␈α∪mathematical␈α∪symmetry.␈α∪ Algol␈α∪60␈α∪requires␈α∪that␈α∪both␈α∪␈↓↓p␈↓␈α∪and␈α∪␈↓↓q␈↓␈α∪be␈α∪computed␈α∩which
␈↓ α∧␈↓precludes␈α∂using␈α∂boolean␈α∂opeators␈α∂as␈α∂the␈α∞main␈α∂connectives␈α∂of␈α∂Lisp␈α∂type␈α∂recursive␈α∂definitions␈α∞of
␈↓ α∧␈↓predicates.

␈↓ α∧␈↓␈↓ αTOther imitation boolean operators are defined by

␈↓ α∧␈↓␈↓ αT␈↓↓p or q = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN T ELSE q␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓not p = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN F ELSE F␈↓.

␈↓ α∧␈↓␈↓ αTWe also require imitations of equality and conditional expressions, namely

␈↓ α∧␈↓␈↓ αT␈↓↓x equal y = IF x = ␈↓πT␈↓↓ ∨ y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF x = y THEN T ELSE F␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN a ELSE b␈↓.

␈↓ α∧␈↓␈↓ αTWe summarize this in the following set of axioms:

␈↓ α∧␈↓␈↓ αT␈↓↓∀p.(istv p ≡ p = T ∨ p = F)␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀p.(isetv p ≡ istv p ∨ p = ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓T ≠ F ∧ ¬istv ␈↓πT␈↓↓␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀p.(isetv p ⊃ not p = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN F ELSE T)␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀p q.(isetv p ∧ isetv q ⊃ p and q = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN q ELSE F)␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀p q.(isetv p ∧ isetv q ⊃ p or q = IF p = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF p = T THEN T ELSE q)␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀X Y.(X equal Y = IF X = ␈↓πT␈↓↓ ∨ Y = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF X = Y THEN T ELSE F␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓∀p␈α
X␈α
Y.(isetv␈α
p␈α
⊃␈α
␈↓αif␈↓↓␈α
p␈α
␈↓αthen␈↓↓␈α
X␈α
␈↓αelse␈↓↓␈α
Y␈α
=␈α
IF␈α
p␈α
=␈α
␈↓πT␈↓↓␈α
THEN␈α
␈↓πT␈↓↓␈α
ELSE␈α
IF␈α
p␈α
=␈α
T␈α
THEN␈α
X
␈↓ α∧␈↓↓ELSE Y␈↓ skip 2 Axioms for Lisp

␈↓ α∧␈↓␈↓ αTAxioms␈α~for␈α~Lisp␈α~are␈α→most␈α~concisely␈α~expressed␈α~in␈α→a␈α~sorted␈α~logic,␈α~and␈α~the␈α→FOL
␈↓ α∧␈↓axiomatizations␈αuse␈αsorts.␈α However,␈αbecause␈αunsorted␈αlogic␈αis␈αmore␈αfamiliar,␈αwe␈αwill␈αuse␈αit␈αat␈αthe
␈↓ α∧␈↓cost␈α∂of␈α∂somewhat␈α∂longer␈α∂axioms.␈α∂ Also␈α∂we␈α∞won't␈α∂assume␈α∂that␈α∂the␈α∂only␈α∂objects␈α∂are␈α∂extended␈α∞S-
␈↓ α∧␈↓expressions,␈α
so␈αthis␈α
axiomatization␈αis␈α
suitable␈α
for␈αuse␈α
when␈αthere␈α
are␈α
other␈αentities␈α
involved␈αin␈α
the
␈↓ α∧␈↓proofs.

␈↓ α∧␈↓L1: ␈↓↓∀x y.(issexp x ∧ issexp y ⊃ issexp(x . y) ∧ ¬isatom(x . y) ∧ ␈↓αa␈↓↓ (x.y) = x ∧ ␈↓αd␈↓↓(x.y) = y)␈↓

␈↓ α∧␈↓L2: ␈↓↓∀x.(issexp x ∧ ¬isatom x ⊃ issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x ∧ ␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x = x)␈↓

␈↓ α∧␈↓L3: ␈↓↓∀u.(islist u ⊃ issexp u)␈↓
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓␈↓ αT L4: ␈↓↓∀u.(u = qNIL ≡ isatom u ∧ islist u)␈↓

␈↓ α∧␈↓L5: ␈↓↓∀u.(islist u ≡ u = qNIL ∨ islist ␈↓αd␈↓↓ u)␈↓

␈↓ α∧␈↓L6: ␈↓↓¬issexp ␈↓πT␈↓↓␈↓

␈↓ α∧␈↓L7: ␈↓↓∀x.(␈↓πT␈↓↓ . x = ␈↓πT␈↓↓ ∧ x . ␈↓πT␈↓↓ = ␈↓πT␈↓↓ ∧ ␈↓αa␈↓↓ ␈↓πT␈↓↓ = ␈↓πT␈↓↓ ∧ ␈↓αd␈↓↓ ␈↓πT␈↓↓ = ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓L8: ␈↓↓∀x.(issexp x ⊃ ␈↓αa␈↓↓t x = IF x = ␈↓πT␈↓↓ THEN ␈↓πT␈↓↓ ELSE IF isatom x THEN T ELSE F)␈↓

␈↓ α∧␈↓␈↓ αTThe predicate ␈↓↓occur[x,y]␈↓ ( which may be read "␈↓↓x␈↓ occurs in ␈↓↓y␈↓" and defined by

␈↓ α∧␈↓␈↓ αT␈↓↓occur[x,y] ← x=y ∨ ¬␈↓αa␈↓↓t y ∧ [occur[x,␈↓αa␈↓↓ y) ∨ occur[x,␈↓αd␈↓↓ y]]␈↓

␈↓ α∧␈↓gives␈αa␈αpartial␈αordering␈αon␈αS-expressions␈αthat␈αcan␈αbe␈αused␈αto␈αprove␈αtermination␈αand␈αis␈αalso␈αused
␈↓ α∧␈↓in␈α∞representing␈α∞recursively␈α∞defined␈α∞functions␈α∞non-recursively␈α
in␈α∞section␈α∞12.␈α∞ We␈α∞will␈α∞write␈α
␈↓↓x ≤ y␈↓
␈↓ α∧␈↓instead of ␈↓↓occur[x,y]␈↓ and axiomatize it by

␈↓ α∧␈↓L9: ␈↓↓∀x y.(issexp x ∧ issexp y ⊃ x ≤ y ≡ x = y ∨ (¬isatom y ∧ (x ≤ ␈↓αa␈↓↓ y ∨ x ≤ ␈↓αd␈↓↓ y)))␈↓

␈↓ α∧␈↓L10: ␈↓↓∀x y.(x < y ≡ x ≤ y ∧ x ≠ y)␈↓

␈↓ α∧␈↓␈↓ αTWith␈αthe␈αaid␈αof␈αthis␈αpartial␈αordering␈αwe␈αcan␈αgive␈αa␈α"course␈αof␈αvalues"␈αscheme␈αfor␈αstructural
␈↓ α∧␈↓induction on S-expressions.  We will discuss induction more systematically later.

␈↓ α∧␈↓L11: ␈↓↓∀x.(issexp x ∧ ∀y.(issexp y ∧ y < x ⊃ qF(y)) ⊃ qF(x)) ⊃ ∀x.(issexp x ⊃ qF(x))␈↓